(*
 * Copyright (c) 2009, Palle Raabjerg
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 *   * Redistributions of source code must retain the above copyright notice,
 *     this list of conditions and the following disclaimer.
 *   * Redistributions in binary form must reproduce the above copyright notice,
 *     this list of conditions and the following disclaimer in the documentation
 *     and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE
 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
 * POSSIBILITY OF SUCH DAMAGE.
 *)

open Printf;;

type label = string;;
type name = string;;
type typevariable = string;;
type effectvariable = string;;

type reso = Reso of label*Spitree.msg
	    | RPair of reso*reso
	    | Empty;;

type env_element = Type of name*typevariable
		   | UnType of name
(*		   | EffectVar of effectvariable*)
		   | Effect of reso;;

type env = (env_element list);;

type basetype = Ch of typevariable
	   | Pair of name*typevariable*typevariable
	   | Un
	   | Key of typevariable
	   | Ok of effectvariable (* Addition to the syntax *)
	   | Abstraction of typevariable*Spitree.msg*typevariable
	   | Application of typevariable*Spitree.msg;;

type typeconstraint = MayEqual of typevariable*basetype
		      | Equal of typevariable*basetype
		      | NotUn of typevariable (* Addition to the syntax *)
		      | Generative of typevariable
		      | NotGenerative of typevariable
		      (*| NotFN of name*Spitree.proc*)
		      | HasType of name*typevariable
		      | Fail;;

type effectconstraint = EffectIncl of label*Spitree.msg*env
			| Instantiates of env*effectvariable
			| InEnv of Spitree.reso*env;;

type envconstraint = WellFormed of env
		     | NamesInDom of Spitree.msg*env
		     | NotInDom of name*env;;

type formula = TypeC of typeconstraint
	       | EffectC of effectconstraint
	       | EnvC of envconstraint
	       | And of formula*formula
	       | Or of formula*formula
	       | Leadsto of formula*formula
	       | Forall of name*formula
	       | Conjunction of (formula list)
	       | CommentConjunction of string*(formula list)
	       | True
;;

let rec string_of_reso reso =
  match reso with
    | Reso(l, m) -> sprintf "%s(%s)" l (Spitree.string_of_msg m)
    | RPair(s1, s2) ->
	sprintf "(%s, %s)" (string_of_reso s1) (string_of_reso s2)
    | Empty -> "Empty"
;;

let string_of_env_element element =
  match element with
    | Type(x, t) -> sprintf "%s:%s" x t
    | UnType(x) -> sprintf "%s:Un" x
    | Effect(reso) -> sprintf "%s" (string_of_reso reso)
;;

let string_of_env env =
  if (List.length env) > 0 then
    "(" ^ (string_of_env_element (List.hd env)) ^
      (List.fold_left (
	 fun envstring element ->
	   envstring ^ ", " ^ (string_of_env_element element)) "" (List.tl env))
    ^ ")"
  else
    "()"
;;
